(set-logic QF_BV)
(declare-fun x () (_ BitVec 6))
(declare-fun y () (_ BitVec 13))
(declare-fun b () Bool)
(assert
  (let((e5 (bvsdiv ((_ sign_extend 7) x) y)))
  (let((e6 ((_ rotate_left 3) x)))
  (let((e7 (bvsrem e6 x)))
  (let((e18 (_ bv1 1)))
  (let((e20 (bvudiv (_ bv0 6) e7)))
  (let((e37 (ite (bvsgt e20 ((_ sign_extend 5) e18)) (_ bv1 1) (_ bv0 1))))
  (let((e44 (bvcomp (_ bv0 13) e5)))
  (let((e175 (bvslt e37 e44)))
  (let((e282 e175))
  (let((e309 (xor e282 true)))
  (let((e313 e309))
  (let((e314 e313))
  (let((e315 (and e314 (not (= e5 (_ bv0 13))))))
  (let((e316 e315))
  (let((e317 e316))
  (let((e318 e317))
  (let((e319 (and e318 b)))
  (let((e320 e319))
  (let((e321 e320)) e321))))))))))))))))))))
(check-sat)